Nuprl Lemma : atom-free-atom2
0,22
postcript
pdf
a
:Atom2. AtomFree(Atom2;
a
)
latex
Definitions
Atom$n
,
t
T
,
AtomFree(
T
;
x
)
,
x
:
A
.
B
(
x
)
origin
a:Atom2. AtomFree(Atom2;a) a:Atom2. AtomFree(Atom2;a) 
Tx:A. B(x)